#pragma once
#include "PDTExpBoolBinBool.h"
#include "PDTBoolConst.h"

class PDTAnd :  public PDTExpBoolBinBool, public TraverseIfc <PDTAnd, PDTNode>  { public:  TRAVERSAL_IFC_IMPL(PDTAnd)
public:
	PDTAnd(PDTCodeGraph & CG, PDTExpBool &left, PDTExpBool & right);
	NodeTypeEnum getType() {
		return PDTAnd_Em;
	}
	bool isAnd() {
		return true;
	}

	virtual bool eval(PDTCodeGraph &CG) //Get the boolean results from the children, AND them,
										//and initialize nValue to a boolean constant with the result
	{
		children[0]->eval(CG);
		children[1]->eval(CG);
		PDTBoolConst* child0 = dynamic_cast<PDTBoolConst*>(children[0]->getNValue());
		PDTBoolConst* child1 = dynamic_cast<PDTBoolConst*>(children[1]->getNValue());
		bool result = child0->getValue() && child1->getValue();
		nValue = new PDTBoolConst(CG, result);
		cout<<"And Result: ("<<child0->getValue()<<") AND ("<<child1->getValue()<<") = "<<result<<endl;
		return true;
	}

	virtual PDTNode* clone(PDTCodeGraph &CG)
	{
		PDTNode* toReturn;
		PDTExpBool* childZeroClone = (PDTExpBool*)(children[0]->clone(CG));
		PDTExpBool* childOneClone = (PDTExpBool*)(children[1]->clone(CG));
		toReturn = new PDTAnd(CG, *childZeroClone, *childOneClone);
		return toReturn;
	}

	virtual stringstream & toString(stringstream & ss) const {
		ss << "( ";
		children[0]->toString(ss) << " And ";
		children[1]->toString(ss) << " )";
		return ss;
	}
	virtual Z3_ast Z3NodeVisit (PDTZ3Visitor &ZV);
};

class PDTOr :  public PDTExpBoolBinBool, public TraverseIfc <PDTOr, PDTNode>  { public:  TRAVERSAL_IFC_IMPL(PDTOr)
public:
	PDTOr(PDTCodeGraph & CG, PDTExpBool &left, PDTExpBool & right);
	NodeTypeEnum getType() {
		return PDTAnd_Em;
	}
	bool isOr() {
		return true;
	}

	virtual bool eval(PDTCodeGraph &CG)
	{
		children[0]->eval(CG);
		children[1]->eval(CG);
		PDTBoolConst* child0 = dynamic_cast<PDTBoolConst*>(children[0]->getNValue());
		PDTBoolConst* child1 = dynamic_cast<PDTBoolConst*>(children[1]->getNValue());
		bool result = child0->getValue() | child1->getValue();
		nValue = new PDTBoolConst(CG, result);
		cout<<"Or Result: ("<<child0->getValue()<<") OR ("<<child1->getValue()<<") = "<<result<<endl;
		return true;
	}

	virtual PDTNode* clone(PDTCodeGraph &CG)
	{
		PDTNode* toReturn;
		PDTExpBool* childZeroClone = (PDTExpBool*)(children[0]->clone(CG));
		PDTExpBool* childOneClone = (PDTExpBool*)(children[1]->clone(CG));
		toReturn = new PDTOr(CG, *childZeroClone, *childOneClone);
		return toReturn;
	}


	virtual stringstream & toString(stringstream & ss) const {
		ss << "( ";
		children[0]->toString(ss) << " Or ";
		children[1]->toString(ss) << " )";
		return ss;
	}
	virtual Z3_ast Z3NodeVisit (PDTZ3Visitor &ZV);
};

class PDTXor :  public PDTExpBoolBinBool, public TraverseIfc <PDTXor, PDTNode> { public:  TRAVERSAL_IFC_IMPL(PDTXor)
public:
	PDTXor(PDTCodeGraph & CG, PDTExpBool &left, PDTExpBool & right);
	NodeTypeEnum getType() {
		return PDTXor_Em;
	}
	bool isXor() {
		return true;
	}

	virtual bool eval(PDTCodeGraph &CG)
	{
		children[0]->eval(CG);
		children[1]->eval(CG);
		PDTBoolConst* child0 = dynamic_cast<PDTBoolConst*>(children[0]->getNValue());
		PDTBoolConst* child1 = dynamic_cast<PDTBoolConst*>(children[1]->getNValue());
		bool result = child0->getValue() ^ child1->getValue();
		nValue = new PDTBoolConst(CG, result);
		cout<<"Xor Result: ("<<child0->getValue()<<") Xor ("<<child1->getValue()<<") = "<<result<<endl;
		return true;
	}

	virtual PDTNode* clone(PDTCodeGraph &CG)
	{
		PDTNode* toReturn;
		PDTExpBool* childZeroClone = (PDTExpBool*)(children[0]->clone(CG));
		PDTExpBool* childOneClone = (PDTExpBool*)(children[1]->clone(CG));
		toReturn = new PDTXor(CG, *childZeroClone, *childOneClone);
		return toReturn;
	}


	virtual stringstream & toString(stringstream & ss) const {
		ss << "( ";
		children[0]->toString(ss) << " Xor ";
		children[1]->toString(ss) << " )";
		return ss;
	}
	virtual Z3_ast Z3NodeVisit (PDTZ3Visitor &ZV);
};

class PDTImplies :  public PDTExpBoolBinBool, public TraverseIfc <PDTImplies, PDTNode> { public:  TRAVERSAL_IFC_IMPL(PDTImplies)
public:
	PDTImplies(PDTCodeGraph & CG, PDTExpBool &left, PDTExpBool & right);
	NodeTypeEnum getType() {
		return PDTImplies_Em;
	}
	bool isImplies() {
	    return true;
	}

	PDTExpBool * getLeft() {
	    return dynamic_cast<PDTExpBool*>(children[0]);
	}

	PDTExpBool * getRight() {
	    return dynamic_cast<PDTExpBool*>(children[1]);
	}

	virtual bool eval(PDTCodeGraph &CG)
	{
	    children[0]->eval(CG);
	    PDTBoolConst* child0 = dynamic_cast<PDTBoolConst*>(children[0]->getNValue());
	    bool result;
	    if (child0->getValue() == false)
	    {
		result = true;
		nValue = new PDTBoolConst(CG, result);
		cout<<"Implication Result: = "<<result<<" since left operand is equal to "<<child0->getValue()<<endl;
	    }
	    else
	    {
		children[1]->eval(CG);
		PDTBoolConst* child1 = dynamic_cast<PDTBoolConst*>(children[1]->getNValue());
		result = child1->getValue();
		nValue = new PDTBoolConst(CG, result);
		cout<<"Implication Result: ("<<child0->getValue()<<") -> ("<<child1->getValue()<<") = "<<result<<endl;
	    }

	    return true;
	}

	virtual PDTNode* clone(PDTCodeGraph &CG)
	{
		PDTNode* toReturn;
		PDTExpBool* childZeroClone = (PDTExpBool*)(children[0]->clone(CG));
		PDTExpBool* childOneClone = (PDTExpBool*)(children[1]->clone(CG));
		toReturn = new PDTImplies(CG, *childZeroClone, *childOneClone);
		return toReturn;
	}


	virtual stringstream & toString(stringstream & ss) const {
		ss << "( ";
		children[0]->toString(ss) << " Implies ";
		children[1]->toString(ss) << " )";
		return ss;
	}
	virtual Z3_ast Z3NodeVisit (PDTZ3Visitor &ZV);
};

class PDTEqualBool :  public PDTExpBoolBinBool, public TraverseIfc <PDTEqualBool, PDTNode> { public:  TRAVERSAL_IFC_IMPL(PDTEqualBool)
public:
	PDTEqualBool(PDTCodeGraph & CG, PDTExpBool &left, PDTExpBool & right);

	NodeTypeEnum getType() {
		return PDTEqualBool_Em;
	}
	bool isEqualBool() {
		return true;
	}

	virtual bool eval(PDTCodeGraph &CG)
	{
		children[0]->eval(CG);
		children[1]->eval(CG);
		PDTBoolConst* child0 = dynamic_cast<PDTBoolConst*>(children[0]->getNValue());
		PDTBoolConst* child1 = dynamic_cast<PDTBoolConst*>(children[1]->getNValue());
		bool result = (child0->getValue() == child1->getValue());
		nValue = new PDTBoolConst(CG, result);
		cout<<"Boolean equal Result: [("<<child0->getValue()<<") == ("<<child1->getValue()<<")] = "<<result<<endl;
		return true;
	}

	virtual PDTNode* clone(PDTCodeGraph &CG)
	{
		PDTNode* toReturn;
		PDTExpBool* childZeroClone = (PDTExpBool*)(children[0]->clone(CG));
		PDTExpBool* childOneClone = (PDTExpBool*)(children[1]->clone(CG));
		toReturn = new PDTEqualBool(CG, *childZeroClone, *childOneClone);
		return toReturn;
	}


	virtual stringstream & toString(stringstream & ss) const {
		ss << "( ";
		children[0]->toString(ss) << " = ";
		children[1]->toString(ss) << " )";
		return ss;
	}
	virtual Z3_ast Z3NodeVisit (PDTZ3Visitor &ZV);
};

class PDTNotEqualBool :  public PDTExpBoolBinBool, public TraverseIfc <PDTNotEqualBool, PDTNode> { public:  TRAVERSAL_IFC_IMPL(PDTNotEqualBool)
public:
	PDTNotEqualBool(PDTCodeGraph & CG, PDTExpBool &left, PDTExpBool & right);

	NodeTypeEnum getType() {
		return PDTNotEqualBool_Em;
	}
	bool isNotEqualBool() {
		return true;
	}

	virtual bool eval(PDTCodeGraph &CG)
	{
		children[0]->eval(CG);
		children[1]->eval(CG);
		PDTBoolConst* child0 = dynamic_cast<PDTBoolConst*>(children[0]->getNValue());
		PDTBoolConst* child1 = dynamic_cast<PDTBoolConst*>(children[1]->getNValue());
		bool result = child0->getValue() != child1->getValue();
		nValue = new PDTBoolConst(CG, result);
		cout<<"Boolean not equal Result: [("<<child0->getValue()<<") != ("<<child1->getValue()<<")] = "<<result<<endl;
		return true;
	}

	virtual PDTNode* clone(PDTCodeGraph &CG)
	{
		PDTNode* toReturn;
		PDTExpBool* childZeroClone = (PDTExpBool*)(children[0]->clone(CG));
		PDTExpBool* childOneClone = (PDTExpBool*)(children[1]->clone(CG));
		toReturn = new PDTNotEqualBool(CG, *childZeroClone, *childOneClone);
		return toReturn;
	}


	virtual stringstream & toString(stringstream & ss) const {
		ss << "( ";
		children[0]->toString(ss) << " != ";
		children[1]->toString(ss) << " )";
		return ss;
	}
	virtual Z3_ast Z3NodeVisit (PDTZ3Visitor &ZV);
};
